\begin{tabbing}
$\forall$${\it es}$:ES, $l_{1}$, $l_{2}$:IdLnk, ${\it tg}_{1}$, ${\it tg}_{2}$:Id.
\\[0ex]es{-}responsive(${\it es}$;$l_{1}$;${\it tg}_{1}$;$l_{2}$;${\it tg}_{2}$)
\\[0ex]$\Rightarrow$ (\=$\exists$$f$:(\{$e$:E$\mid$ kind($e$) $=$ rcv($l_{1}$,${\it tg}_{1}$) $\in$ Knd \}$\rightarrow$\{$e$:E$\mid$ kind($e$) $=$ rcv($l_{2}$,${\it tg}_{2}$) $\in$ Knd \}).\+
\\[0ex]Bij(\{$e$:E$\mid$ kind($e$) $=$ rcv($l_{1}$,${\it tg}_{1}$) $\in$ Knd \}; \{$e$:E$\mid$ kind($e$) $=$ rcv($l_{2}$,${\it tg}_{2}$) $\in$ Knd \}; $f$))
\-
\end{tabbing}